Formal methods form an important branch of software engineering that has apparently been applied to the design of only a small percentage of scientific simulation programs. Two pillars of formalization are specification and verification—that is specifying mathematically what a program must do and verifying the correctness of an algorithm with respect to the specification. The numerical aspects of scientific programming are already formal. The mathematical equations one wishes to solve in a given scientific simulation provide a formal specification, while a proof of numerical convergence provides a formal verification. Hence, formal methods developers often cite a motivation of seeking correctness standards for non-scientific codes as rigorous as those for scientific codes. This ignores, however, the non-numerical aspects of scientific programs that could benefit from greater rigor. One such aspect is memory management.
There have been longstanding calls for increased use of formal methods in scientific programming to improve reliability. Examples of serious common faults include interface inconsistencies and using un-initialized variables.
Adoption of formal methods in scientific simulation has been predicted to be slow because of the requisite mathematical training, which often includes set theory and a predicate calculus. A good candidate for adoption must balance such rigor with ease of use. The Object Constraint Language (OCL) strikes such a balance by facilitating the expression of formal statements about software models without the use of mathematical symbols known only to formal methods specialists. A primary requirement stated by OCL's designers is that OCL must be understood by people who are not mathematicians or computer scientists.
To attract scientific programmers, any software development strategy must address performance. Fortunately, program specification and verification are part of the software design rather than the implementation. Thus, they need not impact run-time performance. However, run-time checking of assertions, a third pillar of formal methods, is part of the implementation. Nonetheless, when the assertions are simple Boolean expressions, they often occupy a negligible fraction of the run time compared to the long loops over millions of floating point calculations typical of scientific software.
A final factor influencing adoption of formal methods is the lack of a common approach for describing the structure of traditional scientific codes beyond flow charts. OCL's incorporation into the recent versions of the Unified Modeling Language (UML), a graphical standard for describing software structure and behavior, suggests that newcomers must simultaneously leap two hurdles: learning OCL and learning UML. Fortunately, increasing interest in object-oriented scientific programming has led to more frequent scientific program structural descriptions resembling UML class models. Class models describe object interfaces and relationships between classes. Object interfaces describe object behavior (procedures) and state (data).
The coupling of OCL and UML class models represents a subtle yet important shift away from the traditional emphases of scientific programming. Traditional approaches develop mathematical abstractions for the physics and the numerics but not the software. For example, continuum mechanics is an abstraction of condensed matter in that it retains only the level of detail required to model macroscopic phenomena. Numerical approximations represent an abstraction of the governing continuum equations in that they retain only the number of discrete values required to obtain a solution within a given tolerance. Likewise, UML class models are software abstractions that retain only the features needed to describe object interfaces and their interrelationships. OCL facilitates describing the resulting software model formally.